natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Syntactic substitution of/for variables is one of the basic operations in formal mathematics, such as in formal logic and type theories, where it is part of the structural rules.
Substitution is usually defined as an operation on expressions (such strings of letters from an alphabet and representing terms, formulas, propositions, dependent types, etc.) containing variables.
Suppose that is an expression in the context of a variable of type, and that is an expression which has the same type as . Then one denotes by
the result of substituting for all occurrences of in .
For example, if is and is , then is .
(substitution is a meta-operation on syntax) In this approach, substitution is an operation on syntax, not an element of syntax itself. In particular, the bracket notation is part of “meta-syntax”, not the syntax in question.
That is, the literal string of symbols “” is not itself an expression in the language under consideration, but denotes such an expression, in the same way that “” is not literally an integer but denotes the numeral “”.
Substitution for multiple variables does not, in general, commute. That is, the expressions
are not in general the same: The former substitutes for occurrences of in , but not for occurrences of in , while the latter has the opposite behavior. We also write
to denote the simultaneous substitution of for and for , in which neither occurrences of in nor occurrences of in are substituted for; this is generally not the same as either iterated substitution.
If the language in question contains variable binders, then there is a subtlety to substitution: if contains free variables that are bound in , then we cannot simply textually substitute for and obtain an expression with the desired meaning.
For instance, if is , and is the free variable , then a literal interpretation of would produce . But is true (universally in its free variables) if the variables have type , while is not. The free variable in has been “captured” by the binder in .
We say that is substitutable for in if performing a literal textual substitution as above would not result in undesired variable capture. If is not substitutable for in , then we can always replace by an alpha-equivalent expression in which is substitutable for . Since we often consider formulas only up to -equivalence anyway, one usually defines the notation “” to include an -conversion of , if necessary, to make substitutable for .
In computer implementations of type theories, however, the issue of variable binding and capture is one of the trickiest things to get right. Performing -conversions is difficult and tedious, and other solutions exist, such as using de Bruijn indices to represent bound variables.
A general property of type theories (and other formal mathematics) is that substitution is an admissible rule.
Roughly, this means that if is an expression of some type, then so is the result of substitution (as long as and have the same type). This is generally not a rule “put into” the theory, but rather a property one proves about the theory; type theorists say that substitution is an admissible rule rather than a derivable rule?.
For instance, in the language of dependent type theory the following substitution rule (one of the structural rules) is an admissible rule:
Here “admissibility” means that if there exist derivations of and , then there also exists a derivation of . By contrast, saying that this is a derivable rule would mean that it can occur itself as part of a derivation, rather than being a meta-statement about derivations.
The substitution rule is closely related to the cut rule, and admissibility of such rules is generally proven by cut elimination.
(alternative typesetting of substitution rule)
In view of Remark we may re-express the substitution rule (1) by using actual syntactic substitutions instead of the meta-instruction “[t/x]” to perform these, if only we make explicit the variable dependency of all terms, say by a subscript:
An alternative approach to substitution is to make substitution part of the object language rather than the metalanguage. That is, the notation
is now actually itself a string of the language under consideration. One then needs reduction or equality rules describing the relationship of this string to the result of actually substituting for as in the usual approach. See explicit substitution for more details.
In the categorical semantics of type theory:
Recalling that terms are interpreted by morphisms, substitution of a term into another term is interpreted by composition of the relevant morphisms.
Recalling that propositions are interpreted by subobjects, substitution of a term into a proposition is interpreted by pullback or inverse image of the subobject interpreting along the morphism interpreting .
Recalling that dependent types are interpreted by display maps, substitution of a term into a dependent type is interpreted by pullback of the display map interpreting along the morphism interpreting .
Or else, since dependent types are also given by classifying morphisms into a type of types, substitution corresponds to composition of these classifying morphisms with the given morphism.
In the third case, there is a coherence issue: syntactic substitution in the usual approach is strictly associative, whereas pullback in a category is not. One way to deal with this is by using explicit substitution as described above. Another way is to strictify the category before modeling type theory; see categorical model of dependent types. For literature see (Curien-Garner-Hofmann, Lumsdaine-Warren 13).
Let be a suitable ambient category in which we are interpreting logic/type theory.
Suppose and are types, hence interpreted as objects of . Then a term of function type is interpreted by a morphism, going by the same symbols.
Now a proposition about terms of type
is interpreted as an object of the slice category , specifically as a (-1)-truncated object if it is to be a proposition, hence by a monomorphism
For instance if Set then this is the inclusion of the subset of elements of on which is true. And generally we may write
Now finally the substitution of for in , hence the proposition
is interpreted as the pullback
Notice that monomorphisms are preserved by pullback, so that this is indeed again the correct interpretation of a proposition.
Specifically, if is the unit type it is interpreted as a terminal object of , and then the function is identified simply with a term . In this case the substitution is evaluation of the proposition at , the resulting monomorphism
over the terminal object is a truth value: the truth value of at .
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
substitution……………………. | pullback of display maps | |
Discussion of the substitution rule in intuitionistic dependent type theory:
Bart Jacobs, p. 123 in: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]
(emphasis on the categorical model of dependent types)
Univalent Foundations Project, p. 423 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
(in the context of homotopy type theory)
Egbert Rijke, p. 4 of: Dependent type theory [pdf], Lecture 1 in: Introduction to Homotopy Type Theory, lecture notes, CMU (2018) [pdf, pdf, webpage]
(in the context of homotopy type theory)
The observation that substitution forms an adjoint pair/adjoint triple with quantifiers is due to
and further developed in
comprehension schema as an adjoint functor_, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.
Exposition of the interpretation of substitution as pullback:
The coherence issue involved in making this precise is discussed in
Pierre-Louis Curien, Richard Garner, Martin Hofmann, Revisiting the categorical interpretation of dependent type theory (pdf)
Peter LeFanu Lumsdaine, Michael Warren, An overlooked coherence construction for dependent type theory, CT2013 (pdf)
Last revised on August 27, 2024 at 13:11:03. See the history of this page for a list of all contributions to it.